package bcontractor.partialmeet;

import static org.hamcrest.Matchers.equalTo;
import static org.hamcrest.Matchers.is;
import static org.junit.Assert.assertThat;

import org.junit.Before;
import org.junit.Test;

import bcontractor.api.ContractionOperator;
import bcontractor.api.SATReasoner;
import bcontractor.api.SentenceSet;
import bcontractor.base.SetUtils;
import bcontractor.propositional.MiniSatReasonerBuilder;
import bcontractor.propositional.PropositionalSentence;
import bcontractor.propositional.SentenceParser;

/**
 * Unit test for FULL partial meet contraction operator
 * 
 * @author lundberg
 * 
 */
public class FullPartialMeetContractionOperatorShould {

    private ContractionOperator<PropositionalSentence> contraction;

    private SATReasoner<PropositionalSentence> reasoner;

    private SentenceParser parser;

    @Before
    public void init() {
        this.contraction = PartialMeetContractionOperatorBuilder.aContractionOperator().build();
        this.reasoner = MiniSatReasonerBuilder.aReasoner().build();
        this.parser = new SentenceParser();
    }

    @Test
    public void stripSentenceStraightforward() {
        SentenceSet<PropositionalSentence> base = this.parser.createSet("a", "b", "a v b");
        PropositionalSentence target = this.parser.create("a");
        SentenceSet<PropositionalSentence> result = this.contraction.eval(base, target);
        assertThat(this.reasoner.entails(result, target), is(false));
        assertThat(result, equalTo(this.parser.createSet("b", "a v b")));
    }

    @Test
    public void stripSentencesThatEntailed() {
        SentenceSet<PropositionalSentence> base = this.parser.createSet("¬a v b", "a", "c");
        PropositionalSentence target = this.parser.create("b");
        SentenceSet<PropositionalSentence> result = this.contraction.eval(base, target);
        assertThat(this.reasoner.entails(result, target), is(false));
        assertThat(result, equalTo(this.parser.createSet("c")));
    }

    @Test
    public void stripSentencesThatWereInvolved() {
        SentenceSet<PropositionalSentence> base = SetUtils.emptySentenceSet();
        base = base.with(this.parser.createList("¬b v a", "b"));
        base = base.with(this.parser.createList("¬b v a", "¬c v ¬d v b", "¬e v d", "c", "e"));
        base = base.with(this.parser.createList("j v k", "m v n v ¬q", "m v ¬n v q v j"));

        PropositionalSentence target = this.parser.create("a");

        SentenceSet<PropositionalSentence> result = this.contraction.eval(base, target);
        assertThat(this.reasoner.entails(result, target), is(false));

        assertThat(result, equalTo(this.parser.createSet("j v k", "m v n v ¬q", "m v ¬n v q v j")));
    }

    @Test
    public void doNothingIfNotNecessary() {
        SentenceSet<PropositionalSentence> base = SetUtils.emptySentenceSet();
        base = base.with(this.parser.createList("¬b v a"));
        base = base.with(this.parser.createList("¬b v a", "¬c v ¬d v b", "¬e v d", "e"));
        base = base.with(this.parser.createList("j v k", "m v n v ¬q", "m v ¬n v q v j"));

        PropositionalSentence target = this.parser.create("a");

        SentenceSet<PropositionalSentence> result = this.contraction.eval(base, target);
        assertThat(this.reasoner.entails(result, target), is(false));

        assertThat(result, equalTo(base));
    }
}
